is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, l2))
↳ QTRS
↳ DependencyPairsProof
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, l2))
IFAPPEND(l1, l2, cons(x, l)) → APPEND(l, l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, l1)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, l2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
IFAPPEND(l1, l2, cons(x, l)) → APPEND(l, l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, l1)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, l2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFAPPEND(l1, l2, cons(x, l)) → APPEND(l, l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, l1)
The value of delta used in the strict ordering is 1.
POL(cons(x1, x2)) = 4 + (4)x_2
POL(IFAPPEND(x1, x2, x3)) = 3 + (4)x_3
POL(APPEND(x1, x2)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, l2))